A, B:Type, b:A+B, f, L1, L2:Top.
map(f;Case b of inl(a)  L1(a) ; inr(a)  L2(a))
~
Case b of inl(a)  map(f;L1(a)) ; inr(a)  map(f;L2(a)) 

latex

Definitions	t  T, Top, x:A. B(x)
Lemmas	top wf